(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const r0 Real)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const r1 Real)
(declare-const v12 Bool)
(declare-const v18 Bool)
(declare-const r7 Real)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const r8 Real)
(declare-const v23 Bool)
(declare-const r9 Real)
(declare-const v24 Bool)
(assert (or (or v12 v22 v12) (or (> (exp r7) (- r7) r7) v22 v10)))
(assert (or (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) (> (exp r7) (- r7) r7) v22) (or v12 v22 v12) (or v10 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v22) (or v10 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0)) (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) (> (exp r7) (- r7) r7) v22) (or (or v12 v22 v12) (or (> (exp r7) (- r7) r7) v22 v10)) (or v12 v10 (> (exp r7) (- r7) r7)) (or (or v12 v12 v10) (or v10 v22 (> (exp r7) (- r7) r7))) (or v22 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v10) (=> (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (or v12 (> (exp r7) (- r7) r7) v12)) (or v12 v12 (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19))))
(assert (and (and (or (<= 0.0 0.0 r0 355036734.0) (<= 0.0 (/ 355036734.0 r0) r0 355036734.0) (> (exp r7) (- r7) r7)) (or v12 (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19) v10) (or (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19) v22 v10) (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v22 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0)) (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (or (> (exp r7) (- r7) r7) v22 v12) (or v22 (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19) v22) (or v12 v10 (> (exp r7) (- r7) r7)) (or v10 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v22)) (or (> (exp r7) (- r7) r7) (> (exp r7) (- r7) r7) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0)) (or (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19) v22 v10) (or (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19) v10 v10) (or (> (exp r7) (- r7) r7) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v22) (or v10 v22 (> (exp r7) (- r7) r7)) (or v10 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v22) (or v12 (> (exp r7) (- r7) r7) v22) (or (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) (> (exp r7) (- r7) r7) v22) (or v12 v22 v12) (or v10 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v22) (or v10 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0)) (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) (> (exp r7) (- r7) r7) v22) (or (or v12 v22 v12) (or (> (exp r7) (- r7) r7) v22 v10)) (or v12 v10 (> (exp r7) (- r7) r7)) (or (or v12 v12 v10) (or v10 v22 (> (exp r7) (- r7) r7))) (or v22 (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v10) (=> (or (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (or v12 (> (exp r7) (- r7) r7) v12)) (or v12 v12 (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19))) (or v12 v12 (distinct v11 v9 v12 (and (=> (distinct 355036734.0 355036734.0 (/ 355036734.0 355036734.0) (/ 355036734.0 355036734.0)) v4) (<= (/ 355036734.0 355036734.0) (/ 355036734.0 r0) r0 355036734.0) v12 v10) (<= r7 (+ r0 (/ 355036734.0 r0) (/ 355036734.0 355036734.0) r0) r1 (- r7) (- r7)) v21 v7 v19)) (or v12 v22 v12)))
(check-sat)
